/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.goal;

import caetus.modelChecking.role.ModelActor;
import caetus.modelChecking.variable.ModelBaseVariable;
import java.util.List;

/**
 *
 * @author Josef Hertl
 */
public class ModelGoalSecret {

    private ModelBaseVariable variableKeptSecret;
    private String secretConstant;
    private List<ModelActor> sharingParties;

    public ModelGoalSecret(ModelBaseVariable variableKeptSecret, String secretConstant, List<ModelActor> sharingParties) {
        this.variableKeptSecret = variableKeptSecret;
        this.secretConstant = secretConstant;
        this.sharingParties = sharingParties;
    }

    /**
     * @param primed Defines if the variable should be primed or not.
     * @return String in format secret(variable,constant,{parties})
     */
    public String makeSecretClause(boolean primed) {
        String result = "secret(" + variableKeptSecret.getVariableName();
        if (primed) {
            result += "'";
        }
        result += "," + secretConstant + ",{";
        for (int i = 0; i < sharingParties.size(); i++) {
            result += sharingParties.get(i).getPlayedByAgent().getVariableName();
            if (i < (sharingParties.size() - 1)) {
                result += ",";
            }
        }
        result += "})";
        return result;
    }

    /**
     * @return The name of the secret constant. Usually it is the same as the
     * name of the secret variable, but in lower case.
     */
    public String getSecretConstant() {
        return secretConstant;
    }

    /**
     * @return The secret variable from this secreat goal.
     */
    public ModelBaseVariable getVariableKeptSecret() {
        return variableKeptSecret;
    }
}
